$\forall$${\it es}$:ES, $e_{1}$, $e_{2}$:E, $P$:(\{$e$:E$\mid$ loc($e$) = loc($e_{1}$) $\in$ Id\} $\rightarrow\mathbb{P}$).
\\[0ex](loc($e_{2}$) = loc($e_{1}$) $\in$ Id) $\Rightarrow$ $\forall$$e$@loc($e_{1}$). Dec($P$($e$)) $\Rightarrow$ Dec($\exists$$e$$\in$[$e_{1}$,$e_{2}$].$P$($e$))